w_locl(w;x;y) == x x,y. first(y) & x = pred(y)^+ y 

latex

---

clarification:

w_locl(w;x;y)
== x 
== rel_plus(w-E(w); (x,y. first(e.w-pred(w;e);y) & x = pred(e.w-pred(w;e);y)  w-E(w))) y 

latex

Definitions	x f y, R^+, A & B, A, b, first(e), s = t, E, pred(e), x.A(x), w-pred(w;e)
FDL editor aliases	w_locl